/*
 * EquivalenceRelation.java
 * 
 * Copyright 2004 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.relations;

import java.util.Hashtable;
import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Set;

import edu.gatech.cc.cnc.Out;
import edu.gatech.cc.cnc.ParseFct;


/**
 * EquivalenceRelation:
 * reflexive, symmetric, and transitive.
 * 
 * Implements an equivalence relation on T.
 * 
 * TODO what are the trade-offs to the standard implementation
 * (according to ``Term rewriting and all that'' by Baader and Nipkow,
 * which is Union/Find, discribed in the dragon book bt Aho, Sethi, and Ullman?
 * 
 * @author csallner@gatech.edu (Christoph Csallner)
 * @version	$Id: $
 */
public class EquivalenceRelation<T> {
	/* Eq is implemented as a powerset construction (p --> {p1, p2, .., pn})
	 * with (p Eq pi). */
	protected final Map<T,Set<T>> eq = new Hashtable<T,Set<T>>();
	
	/**
	 * Get keys
	 */
	public Set<T> getKeys() {
		return eq.keySet();
	}

	
	/**
	 * @return equivalence class containing p, that is,
	 * all params r with (p Eq r).  
	 */
	public Set<T> getEqualValues(T p) {
		assert (p!=null);
		return eq.get(p);
	}
	
	
	/**
	 * @return p1 Eq p2. 
	 */
	public boolean isEqual(T p1, T p2) {
		Set<T> p1Eq = getEqualValues(p1);
		return (p1Eq!=null) && p1Eq.contains(p2);
	}
	
	
	/**
	 * Adds (p, p) to Eq, which thereby remains closed under
	 * reflexivity, symmetry, and transitivity.
	 */
	public void addTuple(T p) {
		assert (p!=null);
		
		if (getEqualValues(p)==null) {
			Set<T> pRange = new LinkedHashSet<T>();
			pRange.add(p);
			eq.put(p, pRange);
		}
		assert isEqual(p, p);  //reflexivity
	}	
	
	
	/**
	 * Adds (p1, p2) to Eq, then closes Eq again under
	 * reflexivity, symmetry, and transitivity.
	 */
	public void addTuple(T p1, T p2) {
		assert (p1!=null);
		assert (p2!=null);

		addTuple(p1); //reflexivity
		addTuple(p2);
		
		/* Symmetry and transitivity */
		T[] p1Eq = (T[]) getEqualValues(p1).toArray();  //equivalent values before
		T[] p2Eq = (T[]) getEqualValues(p2).toArray();
		
		/* eq' := eq union (p1Eq x p2Eq) union (p2Eq x p1Eq) */
		for (T m1: p1Eq) {
			for (T m2: p2Eq) {  					// Add newly equivalent values:
				getEqualValues(m1).add(m2);	// (p1Eq --> p2Eq)
				getEqualValues(m2).add(m1); // (p1Eq <-- p2Eq)
			}
		}
	}
	
	
	
	/**
	 * Replace pOld with pNew in equicalence relation
	 */
	public void replace(T pOld, T pNew) {
		assert pOld!=null;
		assert pNew!=null;
		
		Out.verbose("Replacing "+pOld.toString()+" with "+pNew.toString()+
				" in constraint "+ParseFct.getCnt());
		
		Set<T> pOldEq = getEqualValues(pOld);
		
		if (pOldEq==null) {  //param not previously entered.
			addTuple(pNew);
			return;
		}

		if (pOldEq.size()==1) {  //param exists, but no equivalence constraints.
			eq.remove(pOld);
			addTuple(pNew);
			return;
		}
		
		/* Parm and equivalence constraints exist */
		assert pOldEq.size()>1;
		Out.verbose("Replacing "+pOld.toString()+" in existing constraints");
		
		/* remove pOld from eq */
		pOldEq.remove(pOld);  //other params pOld is equivalent to
		for (T equal: pOldEq) {
			getEqualValues(equal).remove(pOld);
		}
		eq.remove(pOld);
		
		/* Add equivalence to replacement */
		for (T equal: pOldEq) {
			addTuple(pNew, equal);
		}						
	}	
}
